(set-logic QF_NIA)
(declare-fun x_59 () Int)
(declare-fun x_23 () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(define-fun sq_59 () Int (* x_59 x_59))
(push 1)
(assert (= x (ite (= x_23 0) sq_59 (mod sq_59 x_23))))
(assert (= z (ite (or (< (* sq_59 sq_59) 0) (< (* (- 1) (* x x)) 0)) (- x_59) 6)))
(assert (= y (ite (= (* x x) 0) z (div z (* x x)))))
(assert (= (* (abs y) (ite (= (abs y) 0) 1 (div (abs y) (abs y)))) 0))
(check-sat)
(pop 1)
